$\forall$${\it es}$:ES, $a$, $e$:E.
\\[0ex]($\uparrow$isrcv($a$))
\\[0ex]$\Rightarrow$ ($\uparrow$isrcv($e$))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$first(sender($e$))))
\\[0ex]$\Rightarrow$ $a$ $\leq$loc pred(sender($e$)) 
\\[0ex]$\Rightarrow$ (sender($a$) $<$ $e$)